package com.googlecode.kipler.satisfiability.reasoner;

import java.util.Set;

import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.completion.branching.BranchingPoint;
import com.googlecode.kipler.satisfiability.reasoner.profile.ReasoningProfile;
import com.googlecode.kipler.syntax.formula.Formula;

/**
 * This is the generic reasoner interface. It provides a public interface to the
 * tableau algorithm. It supports two main operations which are satisfiability
 * checking of a set of formulas, and determining whether a given formula is
 * logically inferred from a set of formulas.
 * 
 * @author İnanç Seylan
 */
public interface Reasoner {
	/**
	 * Adds a formula to the knowledge base.
	 * 
	 * @param formula
	 */
	public void addFormula(Formula formula);

	/**
	 * Adds a set of formulas to the knowledge base.
	 * 
	 * @param formulas
	 */
	public void addFormulas(Set<Formula> formulas);

	/**
	 * Tells the reasoner to add a branching point for a possible backtracking.
	 * 
	 * @param bp
	 */
	public void addBranch(BranchingPoint bp);

	/**
	 * @return the active {@link WorldConstraintSystem}.
	 */
	public WorldConstraintSystem getCurrentWcs();

	/**
	 * @return the set of options that the reasoner uses.
	 */
	public ReasoningProfile getProfile();
}
